the_w:World.
FairFifo
 (e:E, l:IdLnk. loc(e) = source(l)  Id  sends(l;e) = nil  Msg_sub(l;the_w.M) List) 

latex

Definitions	t  T, x:A. B(x), FairFifo, x:AB(x), E, IdLnk, Id, s = t, A, w.M, Msg_sub(l;M), type List, P  Q, World, b, hd(l), loc(e), x:AB(x), {x:A| B(x) }, A & B, P & Q, source(l), Prop, Void, False, AB, , , time(e), sends(l;e), Msg, P  Q, P  Q, onlnk(l;mss), m(i;t), mlnk(m), a = b, x.A(x), filter(P;l), Msg(M), S  T, Type, haslink(l;m), car.cdr, nil
Lemmas	assert-eq-lnk, haslink wf, assert wf, filter type, eq lnk wf, w-m wf, Msg wf, mlnk wf, Msg sub wf, w-M wf, assert of null, w-Msg wf, not wf, Id wf, w-loc wf, lsrc wf, IdLnk wf, w-E wf, world wf, fair-fifo wf